COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	buggy: fix it!!
C00007 ENDMK
C⊗;
buggy: fix it!!

to write unify(x,y) where x and y are lists containing atoms distinguishable
as either variables or constants. The mgu is returned if x and y are unifable.

want double  loop on x and y.

P{while x∧y do A;x←cdr[x]; y← cdr[y]}Q

using V4 machine should generate:

 P∧(x∧y){A;x←cdr[x]; y←cdr[y]}P P∧¬(x∧y)⊃Q
-------------------------------------------
      P{while x∧y do A;x←cdr[x];y←cdr[y]}Q

and expand it to:

P(x,y)∧(x∧y) {A} P(cdr[x],cdr[y]),  P(x,y)∧¬(x∧y)⊃Q(x,y)
--------------------------------------------------------
P(x,y) {while x∧y do A;x←cdr[x];y←cdr[y]} Q(x,y)

woops! want new variable to contain substitution being built.
want z←NIL followed by loop. machine regroups and does:

P(x,y,z) ⊃ R(x,y,NIL),  R(x,y,z)∧(x∧y){A} R(cdr[x],cdr[y],z), R(x,y,z)∧¬(x∧y)⊃Q(x,y,z)
---------------------------------------------------------------
P(x,y,z){z←NIL;R(x,y,z); while x∧y do A;x←cdr[x];y←cdr[y]}Q(x,y,z)

Now to attack A.

Mumble, perhaps we should try to specify Q first.
Q(x,y,z):  if x and y are not unifiable then z is NIL.
	   otherwise z is a substitution list and z(x)=z(y).

With this, try to specify R in R(x,y,z)∧¬(x∧y)⊃Q(x,y,z).
We can assume that x and y are of the same "length" and thus ¬(x∧y)
means both are empty.
This leads us to modify again. Since R is to be the loop invariant, what is it?
Well it's that z applied to the initial segments of x and y unify them.
So our loop must save  the inputs say in x0 and y0.

Not necessarily: it is only to initial segments  of the inputs which are
of interest.

Observation: at first glance the easiest way to specify invariant
is in terms of two variables say x1, and y1 which contain the initial segments
of x and y and are constructed during the program(by cons). The ONLY reason
for having x1 and y1 is for assertions. Then besides assertions being added
to program we might also add program.

So:
P(x,y,z,x1,y1)⊃R(x,y,z,NIL,NIL,NIL),					(1)
	R(x,y,z,x1,y1)∧(x∧y){A}R(cdr[x],cdr[y],z,car[x].x1,car[y].y1),	(2)
		R(x,y,z,x1,y1)∧¬(x∧y)⊃Q(x,y,z,x1,y1)			(3)
--------------------------------------------------------------------------------
P(x,y,z,x1,y1){z←NIL;x1←NIL;y1←NIL;R(x,y,z,x1,y1);
				   while(x∧y)do A;x1←car[x].x1;
						  y1←car[y].y1;
						  y←cdr[y];x←cdr[x]}Q(x,y,z,x1,y1)}
change Q : x and y are empty; z unifies x1 and y1.

Now a reasonable R is z applied to x1 equals z applied to y1.

Look at (3).We need more information  about x and x1, and y and y1; that
x and y are empty just when x1 and y1 are reverses of the initial x and y.
and that unify(reverse(x),reverse(y)) ↔ unify(x,y);

No it looks like we can simplify things again: Let P be R, then (1) and (3) are 
attainable. (1) is easy and (3) is tedious.

So we have approximately:
z(x1)=z(y1)∧(x∧y) {A} z(car[x].x1)=z(car[y].y1)